Large-scale data centers and cloud computing have turned system configurationinto a challenging problem. Several widely-publicized outages have been blamednot on software bugs, but on configuration bugs. To cope, thousands oforganizations use system configuration languages to manage their computinginfrastructure. Of these, Puppet is the most widely used with thousands ofpaying customers and many more open-source users. The heart of Puppet is adomain-specific language that describes the state of a system. Puppet alreadyperforms some basic static checks, but they only prevent a narrow range oferrors. Furthermore, testing is ineffective because many errors are onlytriggered under specific machine states that are difficult to predict andreproduce. With several examples, we show that a key problem with Puppet isthat configurations can be non-deterministic. This paper presents Rehearsal, a verification tool for Puppet configurations.Rehearsal implements a sound, complete, and scalable determinacy analysis forPuppet. To develop it, we (1) present a formal semantics for Puppet, (2) useseveral analyses to shrink our models to a tractable size, and (3) framedeterminism-checking as decidable formulas for an SMT solver. Rehearsal thenleverages the determinacy analysis to check other important properties, such asidempotency. Finally, we apply Rehearsal to several real-world Puppetconfigurations.
展开▼
